1. Field of the Invention
The invention relates in general to designing integrated circuits, and more particularly, to designing integrated circuit finite state machines.
2. Description of the Related Art
The past decade has seen tremendous growth in the complexity of integrated circuit (IC) designs. Functional verification of IC designs is rapidly becoming one of the most crucial and resource-intensive components of the product design cycle. Conventionally, designs have been verified using extensive simulation. However, simulation-based validation often is insufficient to provide the requisite design coverage needed to expose subtle bugs in increasingly large and complex designs. For many IC designs, only a small fraction of the design's state space can be covered reasonably by simulation. Although formal verification techniques based on binary decision diagrams (BDDs) offer the potential of exhaustive coverage and have met with some success, in practice, the application of BDDs has been limited by the state explosion problem. See, M. Ganai and A. Aziz, “Improved SAT-based Bounded Reachability Analysis,” Proceedings of the 7th ASPDAC/15th International Conference on VLSI Design, pp. 729-734, January 2002; and L. Zhang, M. Prasad and M. Hsiao, “Incremental Deductive & Inductive Reasoning for SAT-based Bounded Model Checking,” Proceedings of IEEE/ACM International Conference on Computer Aided Design, pp. 502-509, November 2004.
Model checking is a verification technique that has been developed to complement simulation-based verification. One of the central problems in synthesis and verification of sequential circuits is reachability analysis. For example, properties to be checked by an automatic verification tool are required to hold in those states that the system can assume after starting in a designated start sate. Reachability analysis is the task of finding this set. Sequential circuits can be modeled as finite state machines (FSM). Reachability analysis typically relies on a traversal of a state transition graph of a FSM. See, K. L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers 1993.
During model checking, an IC design to be verified is modeled as a finite state machine, and a design specification is formalized by writing temporal logic properties. The reachable states of the design are then traversed in order to verify the properties. In case the property fails, a counterexample is generated in the form of a sequence of states leading up to the failure. In general, properties may be classified as ‘safety’ or ‘liveness’ properties. While the former declares what should not happen (or equivalently, what should always happen), the latter declares what should eventually happen. A counterexample to safety properties is a trace of states, where the last state contradicts the property. A counterexample to liveness properties, in its simplest form, is a path to a loop that does not contain the desired state. Such a loop represents an infinite path that never reaches the specified state.
Ordinarily, even the most advanced model checkers are unable to verify all desired properties of a system design in a reasonable amount of time, due to the immense state-spaces of such systems. Model checking can be viewed as finding logical errors (‘falsification’) rather than for proving that they do not exist (‘verification’). Thus, model checking tools typically are used as complementary to the more traditional verification methods involving testing and simulation, and not as an alternative. Often, model checking tools are capable of finding errors that are not likely to be found by simulation. One reason for this is that unlike simulators, which ordinarily examine only a relatively small set of test cases, model checkers may consider virtually all possible behaviors or executions of a system design. Also, the process of writing the temporal properties in a formal language can be quite beneficial by itself, as it clarifies potential ambiguities in an IC design specification. See, A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, Y. Zhu, et al., “Bounded Model Checking,” Advances in Computers, Vol. 58, pp. 117-148, by Elsevier Sciences (USA), 2003.
The basic idea in Bounded Model Checking (BMC) is to search for a counterexample in the executions whose length is bounded by some integer k. Given a temporal logic property p to be verified for a design modeled as a FSM, the basic idea is to search for counterexamples top in the space of all executions of the FSM whose length is bounded by some integer k. This problem is translated into a Boolean formula which is satisfied if and only if a counterexample exists for the given value of k. If no counterexample is found then one increases k until either a counterexample is found, the problem becomes intractable, or some pre-known upper bound is reached. It will be appreciated that correctness of a design, modeled as a FSM, is verified only within a finite number of clock cycles, also known as a ‘bound’.
The check for counterexamples is performed by a satisfiability (SAT) solver. In BMC, the search for counterexamples of increasing length is translated into a sequence of SAT checks. Modern SAT solvers can handle propositional satisfiability problems with hundreds of thousands of variables or more. Significant improvements in SAT solvers have shown that SAT-based BMC often can reason about systems well beyond the capacity limit of BDD-based methods See, A. Biere, et al; and L. Zhang et al.
More specifically, a BMC is an incomplete property checking method that is based on a finite unfolding of a transition relation representing a FSM to disprove the correctness of a set of properties or to prove them for a limited execution lengths from the initial states. FIG. 1 is an illustrative drawing of a sequential circuit implementing a FSM. The FSM has a set of primary inputs x, a set of present state variables s, which are fed by a register, a set of next state variables s′, providing input to the register, and a set of primary outputs y. The FSM implements a combinational logic function in order to produce a set of primary outputs y, and next state values for s′ from a set of primary inputs x for a given set of present state variables s.
A FSM can be expanded into a set of time frames to produce a structural representation of a sequence of FSM states. FIG. 2 is an illustrative drawing showing a temporal expansion of the FSM of FIG. 1 into three time frames. Each time frame replicates the combinational logic of the FSM for each clock cycle being considered. Each time frame includes a copy of the combinational logic implementing a combinational transition function and a corresponding output of the FSM. The circuit structure obtained by this time-frame expansion is a purely combinational structure called transition relation or an iterative logic array (ILA). A transition relation contains no storage elements. Instead, for each frame of an ILA the state variable output values of the transition relation are passed along as inputs to the next frame of the ILA.
BMC techniques repeatedly concatenate a transition relation to unfold an FSM with increasing depths. In the illustrative example of FIG. 2, an initial state s0 is injected at the present state variable s0 of the first time frame. This illustrated sequence of transition relations constitutes a combinational network, which calculates for a given input sequence (x0, x1, x2) the output sequence and next-state response, s3, of the FSM. By applying all input sequences of length three (3) to this circuit, we obtain, at the state variables s3, all possible states the machine can assume at t−3. A temporal expansion of an FSM into t time frames is an implicit representation of the set of states the FSM can assume after exactly t clock ticks. See, D. Stoffel, et al.
BMC has gained significant acceptance in property verification due to its relative robustness in practical applications. Although exhaustive up to the applied bound, BMC does not guarantee completeness, i.e., proving the correctness of a property for depths 0 through k does not necessarily imply that no violation will occur at depths greater than k. Nevertheless, for practical applications BMC has a significant value for refuting properties.
There is a rich set of publications addressing improvements of the original BMC technique. Multiple approaches aim at ensuring completeness, including diameter-based methods, e.g., A. Biere, A. Cimatti, E. M. Clarke and Y. Zhu, “Symbolic model checking without BDDs,” in 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS '99) (Amsterdam, Netherlands) pp. 193-207, March 1999; J. Baumgartner, A. Kuehlmann and J. Abraham, “Property checking via structural analysis,” in Computer-Aided Verification (CAV '02), (Copenhagen, Denmark), pp. 151-165, January 2003; and D. Koening and O. Strichman, “Efficient computation of recurrence diameters,” in International Conference for Verification, Model Checking, and Abstract Interpretation, January 2003, abstraction-based techniques that combine BMC with classical symbolic model checking, e.g., P. Chauhan, E. Clarke, J. Kukula, S. Sapra and D. Wang, “Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis,” in Formal Methods of Computer Aided Design (FMCAD '02), pp. 33-51, Springer-Verlag, November 2002; and K. L. McMillan and N. Amla, “Automated abstraction without counterexamples,”, in International Conference on tools and Algorithms for Construction and Analysis of Systems (TACAS '03), (Warsaw, Poland), pp. 2-17, April 2003 LNCS 2619, and inductive methods that can prove correctness of k-step inductive properties as part of the BMC unfolding e.g., M. Sheeran, S. Singh and G. Stalmarck, “Checking safety properties using induction and a SAT-solver,” in Formal Methods in Computer-Aided Design (Austin, Tex.), pp. 108-125, Springer-Verlag, November 2000. Other works improve the SAT engine itself and address efficient encoding schemes e.g., A. Gupta, Z. Yang and P. Ashar, “Dynamic Detection and removal of inactive clauses in SAT-solver,” in 38th Design Automation Conference Proceedings (Las Vegas, Nev.), 2001.
AND/INVERTER graphs (AIGs) were previously proposed for use in design verification in A. Kuehlmann and F. Krohm, “Equivalence Checking Using Cuts and Heaps,” in Proceedings of the 34th ACM/IEEE Design Automation Conference, (Anaheim, Calif.), pp. 263-268, June 1997; and A. Kuehlmann, V. Paruthi, F. Krohm and M. K. Ganai, “Robust Boolean Reasoning for Equivalence Checking and Functional Property Verification,” IEEE Transactions on Computer-” Aided Design, vol. 21, pp. 1377-1394, December 2002. In M. Ganai and A. Aziz, “Improved SAT-based Bounded Reachability Analysis,” Proceedings of the 7th ASPDAC/15th International Conference on VLSI Design, pp. 729-734, January 2002, AIGs also were applied for BMC with the specific improvement to assert previously proved properties at past time frames in the BMC unfolding. Also, see M. Sheeran, S. Singh and G. Stalmarck, “Checking safety properties using induction and a SAT-solver,” in Formal Methods in Computer-Aided Design (Austin, Tex.), pp. 108-125, Springer-Verlag, November 2000. This prior work and others (e.g. See, A. Kuehlmann, V. Paruthi, F. Krohm and M. K. Ganai, “Robust Boolean Reasoning for Equivalence Checking and Functional Property Verification,” IEEE Transactions on Computer-” Aided Design, vol. 21, pp. 1377-1394, December 2002; and P. Bjesse and K. Claessen, “SAT-based verification without state space traversal,” in Formal Methods in Computer-Aided Design (FMCAD '00), (Austin, Tex.), pp. 372-389, Springer-Verlag, November 2000) apply simplification for a BMC unfolding.
Moreover, a BMC unfolding may include transition relations that have unreachable states. An unreachable state is a state that becomes unreachable after some number of transitions of a finite state machine. FIG. 3A is an illustrative drawing of a state transition diagram for a finite state machine (not shown) that includes states S1-S5 in which state S1 becomes unreachable after one state transition. In other words, no matter what state the finite state machine starts out from, state S1 will be unreachable after the first state transition. FIG. 3B is an illustrative drawing of a state transition diagram of a different finite state machine (not shown) including states R1-R5 in which state R1 becomes unreachable after one state transition, and state R2 becomes unreachable after two state transitions. No matter what state the finite state machine starts out from, state R1 will be unreachable after the first state transition, and R2 will be unreachable after the second state transition. BMC for unreachable states is unnecessary and wasteful of computing resources. Thus, there has been a need to identify and eliminate the checking of unreachable states from a BMC unfolding.
Unfortunately, due to the initialization, the time frames of a BMC unfolding are unique and their simplification cannot be reused for later frames. As a result, a significant amount of redundant work was performed repeatedly during each BMC step, e.g., to discover that two AND vertices are invariantly equivalent after a few transitions. Moreover, proving the same equivalence in subsequent BMC unfolding frames typically requires a growing reasoning effort due to the enlarging formula depth.
One earlier method of simplification of BMC unfolding frames reuses clauses of a formula in Conjunctive Normal Form (CNF) which are learned during earlier BMC steps for future unfoldings. See, O. Shtrichman, “Pruning techniques for the SAT-based bounded model checking problem,” in Correct Hardware Design and Verification Methods (CHARME' '01), (Livingston, Scotland), pp. 58-70, Springer-Verlag, September 2001. However, the proposed reuse method is restricted to a CNF-based representation and basically copies learned clauses from previous frames.
There also has been a need for improvements in finite state machines with states that become unreachable after some number of time frames. In such machines, certain logic that relates to states that become unreachable after the initial time frames is not necessary after the states become unreachable. The presence of such unnecessary logic in later time frames can reduce the potential of speed and efficiency of the machine in later time frames when unreachable states have become unreachable.
Thus, there has been a need for improvements in BMC. There also has been a need for improvements in finite state machines to reduce inefficiencies associated with unreachable states. The present invention meets these needs.